es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id} ). e@loc(e'). Dec(P(e))  Dec(e<e'.P(e)) 

latex

Definitions

x:A. B(x), t  T, , P  Q, x(s), x. t(x), A c B, P  Q, b, tt, if b then t else f fi , ff, Dec(P), A, True, {T}, WellFnd{i}(A;x,y.R(x;y)), P  Q, P  Q, P & Q, , Unit, False, e@i. P(e),

Lemmas

event system wf, es-locl-wellfnd, event system-level-subtype, es-E wf, Id wf, es-loc wf, alle-at wf, decidable wf, existse-before wf, es-locl wf, decidable functionality, not wf, assert wf, es-first wf, es-pred wf, es-loc-pred, existse-before-iff, bool wf, eqtt to assert, iff transitivity, bnot wf, eqff to assert, assert of bnot, true wf, decidable and, false wf, decidable not, decidable false, decidable or, es-pred-locl